es:ES, x, i:Id, T:Type.
(x, y:T. Dec(x = y  T))
 @i(x:T)
 (e', e:E.
 (e <loc e')
  (loc(e') = i)
  (((x after e) = (x when e')  T))
  (ev:E
  (((e <loc ev) & (ev <loc e')
  (& (((x after ev) = (x when ev)  T))
  (& (x after ev) = (x when e')  T))) 

latex

Definitions	True, T, A, A c B, P & Q, x:A. B(x), P  Q, , (e <loc e'), t  T, x:A. B(x), False, P  Q, Dec(P), P  Q, @i(x:T)
Lemmas	es-E wf, true wf, squash wf, es-le weakening, es-locl transitivity2, es-after-pred2, decidable es-locl, es-pred-locl, es-pred wf, event system wf, decidable wf, es-dtype wf, es-locl wf, es-when wf, es-vartype wf, es-locl-iff, es-loc-pred, es-after wf, not wf, es-causl wf, es-loc wf, Id wf